\begin{tabbing}
es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$$\in$fpf{-}domain(${\it ds}$).let $T$ = fpf{-}ap(${\it ds}$; IdDeq; $x$) in es{-}vartype(${\it es}$; $i$; $x$) $\subseteq\rho$ $T$\+
\\[0ex]\& $\forall$\=$k$$\in$fpf{-}domain(${\it da}$).\+
\\[0ex]let $T$ = fpf{-}ap(${\it da}$; KindDeq; $k$) in 
\\[0ex]$\forall$$e$:es{-}E(${\it es}$).
\\[0ex]es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id $\vee$ es{-}isrcv(${\it es}$; $e$)
\\[0ex]$\Rightarrow$ es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$
\-\-
\end{tabbing}